\begin{tabbing}
w{-}pred($w$;$e$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=i\=f w{-}time($w$; $e$)=$_{2}$0$\rightarrow$ inr($\cdot$)\+\+
\\[0ex]; \=w{-}isnull($w$; w{-}a($w$; w{-}loc($w$; $e$); (w{-}time($w$; $e$)$-$1)))$\rightarrow$\+
\\[0ex]w{-}pred($w$;$\langle$w{-}loc($w$; $e$)$,\,$w{-}time($w$; $e$)$-$1$\rangle$)
\-\-\\[0ex]else inl($\langle$w{-}loc($w$; $e$)$,\,$w{-}time($w$; $e$)$-$1$\rangle$) fi
\-\\[0ex]\emph{(recursive)}
\end{tabbing}